(* ========================================================================= *)
(* Arithmetization of syntax and Tarski's theorem.                           *)
(* ========================================================================= *)

prioritize_num();;

(* ------------------------------------------------------------------------- *)
(* This is to fake the fact that we might really be using strings.           *)
(* ------------------------------------------------------------------------- *)

let number = new_definition
 `number(x) = 2 * (x DIV 2) + (1 - x MOD 2)`;;
let denumber = new_definition
 `denumber = number`;;
let NUMBER_DENUMBER = 
prove (`(!s. denumber(number s) = s) /\ (!n. number(denumber n) = n)`,
REWRITE_TAC[number; denumber] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN SIMP_TAC[ARITH_RULE `x < 2 ==> (2 * y + x) DIV 2 = y`; MOD_MULT_ADD; MOD_LT; GSYM DIVISION; ARITH_EQ; ARITH_RULE `1 - m < 2`; ARITH_RULE `x < 2 ==> 1 - (1 - x) = x`]);;
let NUMBER_INJ = 
prove (`!x y. number(x) = number(y) <=> x = y`,
MESON_TAC[NUMBER_DENUMBER]);;
let NUMBER_SURJ = 
prove (`!y. ?x. number(x) = y`,
MESON_TAC[NUMBER_DENUMBER]);;
(* ------------------------------------------------------------------------- *) (* Arithmetization. *) (* ------------------------------------------------------------------------- *)
let gterm = new_recursive_definition term_RECURSION
  `(gterm (V x) = NPAIR 0 (number x)) /\
   (gterm Z = NPAIR 1 0) /\
   (gterm (Suc t) = NPAIR 2 (gterm t)) /\
   (gterm (s ++ t) = NPAIR 3 (NPAIR (gterm s) (gterm t))) /\
   (gterm (s ** t) = NPAIR 4 (NPAIR (gterm s) (gterm t)))`;;
let gform = new_recursive_definition form_RECURSION
  `(gform False = NPAIR 0 0) /\
   (gform True = NPAIR 0 1) /\
   (gform (s === t) = NPAIR 1 (NPAIR (gterm s) (gterm t))) /\
   (gform (s << t) = NPAIR 2 (NPAIR (gterm s) (gterm t))) /\
   (gform (s <<= t) = NPAIR 3 (NPAIR (gterm s) (gterm t))) /\
   (gform (Not p) = NPAIR 4 (gform p)) /\
   (gform (p && q) = NPAIR 5 (NPAIR (gform p) (gform q))) /\
   (gform (p || q) = NPAIR 6 (NPAIR (gform p) (gform q))) /\
   (gform (p --> q) = NPAIR 7 (NPAIR (gform p) (gform q))) /\
   (gform (p <-> q) = NPAIR 8 (NPAIR (gform p) (gform q))) /\
   (gform (!! x p) = NPAIR 9 (NPAIR (number x) (gform p))) /\
   (gform (?? x p) = NPAIR 10 (NPAIR (number x) (gform p)))`;;
(* ------------------------------------------------------------------------- *) (* Injectivity. *) (* ------------------------------------------------------------------------- *)
let GTERM_INJ = 
prove (`!s t. (gterm s = gterm t) <=> (s = t)`,
MATCH_MP_TAC term_INDUCT THEN REPEAT CONJ_TAC THENL [ALL_TAC; GEN_TAC; GEN_TAC THEN DISCH_TAC; REPEAT GEN_TAC THEN STRIP_TAC; REPEAT GEN_TAC THEN STRIP_TAC] THEN MATCH_MP_TAC term_INDUCT THEN ASM_REWRITE_TAC[term_DISTINCT; term_INJ; gterm; NPAIR_INJ; NUMBER_INJ; ARITH_EQ]);;
let GFORM_INJ = 
prove (`!p q. (gform p = gform q) <=> (p = q)`,
MATCH_MP_TAC form_INDUCT THEN REPEAT CONJ_TAC THENL [ALL_TAC; ALL_TAC; GEN_TAC THEN GEN_TAC; GEN_TAC THEN GEN_TAC; GEN_TAC THEN GEN_TAC; REPEAT GEN_TAC THEN STRIP_TAC; REPEAT GEN_TAC THEN STRIP_TAC; REPEAT GEN_TAC THEN STRIP_TAC; REPEAT GEN_TAC THEN STRIP_TAC; REPEAT GEN_TAC THEN STRIP_TAC; REPEAT GEN_TAC THEN STRIP_TAC; REPEAT GEN_TAC THEN STRIP_TAC] THEN MATCH_MP_TAC form_INDUCT THEN ASM_REWRITE_TAC[form_DISTINCT; form_INJ; gform; NPAIR_INJ; ARITH_EQ] THEN REWRITE_TAC[GTERM_INJ; NUMBER_INJ]);;
(* ------------------------------------------------------------------------- *) (* Useful case theorems. *) (* ------------------------------------------------------------------------- *)
let GTERM_CASES = 
prove (`((gterm u = NPAIR 0 (number x)) <=> (u = V x)) /\ ((gterm u = NPAIR 1 0) <=> (u = Z)) /\ ((gterm u = NPAIR 2 n) <=> (?t. (u = Suc t) /\ (gterm t = n))) /\ ((gterm u = NPAIR 3 (NPAIR m n)) <=> (?s t. (u = s ++ t) /\ (gterm s = m) /\ (gterm t = n))) /\ ((gterm u = NPAIR 4 (NPAIR m n)) <=> (?s t. (u = s ** t) /\ (gterm s = m) /\ (gterm t = n)))`,
STRUCT_CASES_TAC(SPEC `u:term` term_CASES) THEN ASM_REWRITE_TAC[gterm; NPAIR_INJ; ARITH_EQ; NUMBER_INJ; term_DISTINCT; term_INJ] THEN MESON_TAC[]);;
let GFORM_CASES = 
prove (`((gform r = NPAIR 0 0) <=> (r = False)) /\ ((gform r = NPAIR 0 1) <=> (r = True)) /\ ((gform r = NPAIR 1 (NPAIR m n)) <=> (?s t. (r = s === t) /\ (gterm s = m) /\ (gterm t = n))) /\ ((gform r = NPAIR 2 (NPAIR m n)) <=> (?s t. (r = s << t) /\ (gterm s = m) /\ (gterm t = n))) /\ ((gform r = NPAIR 3 (NPAIR m n)) <=> (?s t. (r = s <<= t) /\ (gterm s = m) /\ (gterm t = n))) /\ ((gform r = NPAIR 4 n) = (?p. (r = Not p) /\ (gform p = n))) /\ ((gform r = NPAIR 5 (NPAIR m n)) <=> (?p q. (r = p && q) /\ (gform p = m) /\ (gform q = n))) /\ ((gform r = NPAIR 6 (NPAIR m n)) <=> (?p q. (r = p || q) /\ (gform p = m) /\ (gform q = n))) /\ ((gform r = NPAIR 7 (NPAIR m n)) <=> (?p q. (r = p --> q) /\ (gform p = m) /\ (gform q = n))) /\ ((gform r = NPAIR 8 (NPAIR m n)) <=> (?p q. (r = p <-> q) /\ (gform p = m) /\ (gform q = n))) /\ ((gform r = NPAIR 9 (NPAIR (number x) n)) <=> (?p. (r = !!x p) /\ (gform p = n))) /\ ((gform r = NPAIR 10 (NPAIR (number x) n)) <=> (?p. (r = ??x p) /\ (gform p = n)))`,
STRUCT_CASES_TAC(SPEC `r:form` form_CASES) THEN ASM_REWRITE_TAC[gform; NPAIR_INJ; ARITH_EQ; NUMBER_INJ; form_DISTINCT; form_INJ] THEN MESON_TAC[]);;
(* ------------------------------------------------------------------------- *) (* Definability of "godel number of numeral n". *) (* ------------------------------------------------------------------------- *)
let gnumeral = new_definition
  `gnumeral m n = (gterm(numeral m) = n)`;;
let arith_gnumeral1 = new_definition
 `arith_gnumeral1 a b = formsubst ((3 |-> a) ((4 |-> b) V))
       (??0 (??1
       (V 3 === arith_pair (V 0) (V 1) &&
        V 4 === arith_pair (Suc(V 0)) (arith_pair (numeral 2) (V 1)))))`;;
let ARITH_GNUMERAL1 = 
prove (`!v a b. holds v (arith_gnumeral1 a b) <=> ?x y. termval v a = NPAIR x y /\ termval v b = NPAIR (SUC x) (NPAIR 2 y)`,
let FV_GNUMERAL1 = 
prove (`!s t. FV(arith_gnumeral1 s t) = FVT s UNION FVT t`,
REWRITE_TAC[arith_gnumeral1] THEN FV_TAC[FVT_PAIR; FVT_NUMERAL]);;
let arith_gnumeral1' = new_definition
 `arith_gnumeral1' x y = arith_rtc arith_gnumeral1 x y`;;
let ARITH_GNUMERAL1' = 
prove (`!v s t. holds v (arith_gnumeral1' s t) <=> RTC (\a b. ?x y. a = NPAIR x y /\ b = NPAIR (SUC x) (NPAIR 2 y)) (termval v s) (termval v t)`,
REWRITE_TAC[arith_gnumeral1'] THEN MATCH_MP_TAC ARITH_RTC THEN REWRITE_TAC[ARITH_GNUMERAL1]);;
let FV_GNUMERAL1' = 
prove (`!s t. FV(arith_gnumeral1' s t) = FVT s UNION FVT t`,
SIMP_TAC[arith_gnumeral1';
FV_RTC; FV_GNUMERAL1]);;
let arith_gnumeral = new_definition
 `arith_gnumeral n p =
        formsubst ((0 |-> n) ((1 |-> p) V))
            (arith_gnumeral1' (arith_pair Z (numeral 3))
                              (arith_pair (V 0) (V 1)))`;;
let ARITH_GNUMERAL = 
prove (`!v s t. holds v (arith_gnumeral s t) <=> gnumeral (termval v s) (termval v t)`,
REWRITE_TAC[arith_gnumeral; holds; HOLDS_FORMSUBST; ARITH_GNUMERAL1';
ARITH_PAIR; TERMVAL_NUMERAL] THEN REWRITE_TAC[termval; ARITH_EQ; o_THM; valmod] THEN MP_TAC(INST [`(gterm o numeral)`,`fn:num->num`; `3`,`e:num`; `\a:num b:num. NPAIR 2 a`,`f:num->num->num`] PRIMREC_SIGMA) THEN ANTS_TAC THENL [REWRITE_TAC[gterm; numeral; o_THM] THEN REWRITE_TAC[NPAIR; ARITH]; SIMP_TAC[gnumeral; o_THM]]);;
let FV_GNUMERAL = 
prove (`!s t. FV(arith_gnumeral s t) = FVT(s) UNION FVT(t)`,
REWRITE_TAC[arith_gnumeral] THEN FV_TAC[FV_GNUMERAL1';
FVT_PAIR; FVT_NUMERAL]);; (* ------------------------------------------------------------------------- *) (* Diagonal substitution. *) (* ------------------------------------------------------------------------- *)
let qdiag = new_definition
  `qdiag x q = qsubst (x,numeral(gform q)) q`;;
let arith_qdiag = new_definition
  `arith_qdiag x s t =
        formsubst ((1 |-> s) ((2 |-> t) V))
        (?? 3
           (arith_gnumeral (V 1) (V 3) &&
            arith_pair (numeral 10)  (arith_pair (numeral(number x))
                                                 (arith_pair (numeral 5)
              (arith_pair (arith_pair (numeral 1)
       (arith_pair (arith_pair (numeral 0) (numeral(number x))) (V 3)))
                   (V 1)))) ===
        V 2))`;;
let QDIAG_FV = 
prove (`FV(qdiag x q) = FV(q) DELETE x`,
let HOLDS_QDIAG = 
prove (`!v x q. holds v (qdiag x q) = holds ((x |-> gform q) v) q`,
let ARITH_QDIAG = 
prove (`(termval v s = gform p) ==> (holds v (arith_qdiag x s t) <=> (termval v t = gform(qdiag x p)))`,
REPEAT STRIP_TAC THEN REWRITE_TAC[qdiag; qsubst; arith_qdiag; gform; gterm] THEN ASM_REWRITE_TAC[HOLDS_FORMSUBST; holds; termval; TERMVAL_NUMERAL; gnumeral; ARITH_GNUMERAL; ARITH_PAIR] THEN ASM_REWRITE_TAC[o_DEF; valmod; ARITH_EQ; termval] THEN MESON_TAC[]);;
let FV_QDIAG = 
prove (`!x s t. FV(arith_qdiag x s t) = FVT(s) UNION FVT(t)`,
REWRITE_TAC[arith_qdiag; FORMSUBST_FV; FV; FV_GNUMERAL; FVT_PAIR; UNION_EMPTY; FVT_NUMERAL; FVT; TERMSUBST_FVT] THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN REWRITE_TAC[DISJ_ACI; IN_DELETE; IN_UNION; IN_SING] THEN REWRITE_TAC[TAUT `(a \/ b) /\ c <=> a /\ c \/ b /\ c`] THEN REWRITE_TAC[EXISTS_OR_THM; GSYM CONJ_ASSOC; UNWIND_THM2; ARITH_EQ] THEN REWRITE_TAC[valmod; ARITH_EQ; DISJ_ACI]);;
(* ------------------------------------------------------------------------- *) (* Hence diagonalization of a predicate. *) (* ------------------------------------------------------------------------- *)
let diagonalize = new_definition
  `diagonalize x q =
        let y = VARIANT(x INSERT FV(q)) in
        ??y (arith_qdiag x (V x) (V y) && formsubst ((x |-> V y) V) q)`;;
let FV_DIAGONALIZE = 
prove (`!x q. FV(diagonalize x q) = x INSERT (FV q)`,
REPEAT GEN_TAC THEN REWRITE_TAC[diagonalize] THEN LET_TAC THEN REWRITE_TAC[FV; FV_QDIAG; FORMSUBST_FV; EXTENSION; IN_INSERT; IN_DELETE; IN_UNION; IN_ELIM_THM; FVT; NOT_IN_EMPTY] THEN X_GEN_TAC `u:num` THEN SUBGOAL_THEN `~(y = x) /\ !z. z IN FV(q) ==> ~(y = z)` STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[VARIANT_FINITE; FINITE_INSERT; FV_FINITE; IN_INSERT]; ALL_TAC] THEN ASM_CASES_TAC `u:num = x` THEN ASM_REWRITE_TAC[] THEN ASM_CASES_TAC `u:num = y` THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[valmod; COND_RAND; FVT; IN_SING; COND_EXPAND] THEN ASM_MESON_TAC[]);;
let ARITH_DIAGONALIZE = 
prove (`(v x = gform p) ==> !q. holds v (diagonalize x q) <=> holds ((x |-> gform(qdiag x p)) v) q`,
REPEAT STRIP_TAC THEN REWRITE_TAC[diagonalize] THEN LET_TAC THEN REWRITE_TAC[holds] THEN SUBGOAL_THEN `!a. holds ((y |-> a) v) (arith_qdiag x (V x) (V y)) <=> (termval ((y |-> a) v) (V y) = gform(qdiag x p))` (fun th -> REWRITE_TAC[th]) THENL [GEN_TAC THEN MATCH_MP_TAC ARITH_QDIAG THEN REWRITE_TAC[termval; valmod] THEN SUBGOAL_THEN `~(x:num = y)` (fun th -> ASM_REWRITE_TAC[th]) THEN ASM_MESON_TAC[VARIANT_FINITE; FINITE_INSERT; FV_FINITE; IN_INSERT]; ALL_TAC] THEN REWRITE_TAC[HOLDS_FORMSUBST; termval; VALMOD_BASIC; UNWIND_THM2] THEN MATCH_MP_TAC HOLDS_VALUATION THEN X_GEN_TAC `u:num` THEN DISCH_TAC THEN REWRITE_TAC[o_THM; termval; valmod] THEN COND_CASES_TAC THEN REWRITE_TAC[termval] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[VARIANT_FINITE; FINITE_INSERT; FV_FINITE; IN_INSERT]);;
(* ------------------------------------------------------------------------- *) (* And hence the fixed point. *) (* ------------------------------------------------------------------------- *)
let fixpoint = new_definition
  `fixpoint x q = qdiag x (diagonalize x q)`;;
let FV_FIXPOINT = 
prove (`!x p. FV(fixpoint x p) = FV(p) DELETE x`,
REWRITE_TAC[fixpoint; FV_QDIAG; QDIAG_FV; FV_DIAGONALIZE; FVT_NUMERAL] THEN SET_TAC[]);;
let HOLDS_FIXPOINT = 
prove (`!x p v. holds v (fixpoint x p) <=> holds ((x |-> gform(fixpoint x p)) v) p`,
REPEAT GEN_TAC THEN SIMP_TAC[fixpoint; holds; HOLDS_QDIAG] THEN SUBGOAL_THEN `((x |-> gform(diagonalize x p)) v) x = gform (diagonalize x p)` MP_TAC THENL [REWRITE_TAC[VALMOD_BASIC]; ALL_TAC] THEN DISCH_THEN(fun th -> REWRITE_TAC[MATCH_MP ARITH_DIAGONALIZE th]) THEN REWRITE_TAC[VALMOD_VALMOD_BASIC]);;
let HOLDS_IFF_FIXPOINT = 
prove (`!x p v. holds v (fixpoint x p <-> qsubst (x,numeral(gform(fixpoint x p))) p)`,
let CARNAP = 
prove (`!x q. ?p. (FV(p) = FV(q) DELETE x) /\ true (p <-> qsubst (x,numeral(gform p)) q)`,
REPEAT GEN_TAC THEN EXISTS_TAC `fixpoint x q` THEN REWRITE_TAC[true_def; HOLDS_IFF_FIXPOINT; FV_FIXPOINT]);;
(* ------------------------------------------------------------------------- *) (* Hence Tarski's theorem on the undefinability of truth. *) (* ------------------------------------------------------------------------- *)
let definable_by = new_definition
  `definable_by P s <=> ?p x. P p /\ (!v. holds v p <=> (v(x)) IN s)`;;
let definable = new_definition
  `definable s <=> ?p x. !v. holds v p <=> (v(x)) IN s`;;
let TARSKI_THEOREM = 
prove (`~(definable {gform p | true p})`,
REWRITE_TAC[definable; IN_ELIM_THM; NOT_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`p:form`; `x:num`] THEN DISCH_TAC THEN MP_TAC(SPECL [`x:num`; `Not p`] CARNAP) THEN DISCH_THEN(X_CHOOSE_THEN `q:form` (MP_TAC o CONJUNCT2)) THEN SIMP_TAC[true_def; holds; HOLDS_QSUBST; FVT_NUMERAL; NOT_IN_EMPTY] THEN ONCE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[VALMOD_BASIC; TERMVAL_NUMERAL] THEN REWRITE_TAC[true_def; GFORM_INJ] THEN MESON_TAC[]);;
(* ------------------------------------------------------------------------- *) (* Misc. stuff to sanity-check the book. *) (* ------------------------------------------------------------------------- *) (***** let pairpair = new_definition `pair(x,y) = NPAIR x y`;; let BREAK = rand o concl o (ONCE_REWRITE_CONV[gform; gterm] THENC REWRITE_CONV[GSYM pairpair]);; let tm0 = `gform(?? x (V x === k && p))`;; let tm1 = BREAK tm0;; let tm2 = BREAK tm1;; let tm3 = BREAK tm2;; let tm4 = BREAK tm3;; ******)